r:. ((r = 0  ))  (qpositive(|r|)) 

latex

Definitions	, ff, tt, t  T, if b then t else f fi , |r|, P  Q, x:A. B(x), False, P & Q, P  Q, Unit, , P  Q, A, S  T,
Lemmas	int inc rationals, rationals wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, qpositive wf, q trichotomy